T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
(x changed before e)
 (es-locl(es; (last change to x before e); e)
 c (@(last change to x before e)(xes-when(es; x; e))
 c  e''((last change to x before e),e].es-when(es; x; e'') = es-when(es; x; e)  T)) 

latex

Definitions	if b then t else f fi , ff, tt, outl(x), t.1, isl(x), b, A c B, x. t(x), P  Q, P  Q, es-dtype(es; i; x; T), EqDecider(T), prop{i:l}, P  Q, t  T, change-to(x;e), P  Q, (last change to x before e), x changed before e, P  Q, x:A. B(x), x:A. B(x), False, e<e'.P(e), x(s)
Lemmas	false wf, true wf, alle-le wf, es-first wf, not wf, alle-between3 wf, es-when wf, es-change-to wf, existse-before wf, es-vartype wf, es-isconst wf, iff wf, bool wf, deq wf, event system wf, Id wf, es-loc wf, es-dtype wf, change-to wf, unit wf, es-E wf, isl wf, assert wf